package minsat;

import java.util.ArrayList;
import java.util.List;

/**
 * Represents a single clause in the MinSat instance which has a given weight, is either hard or
 * soft, and contains a list of arbitrarily many Literals.
 */
public class Clause
{
  public final List<Literal> literals;
  public final Double weight;

  /**
   * Copy constructor for Clause
   */
  public Clause(Clause c)
  {
    this.literals = new ArrayList<Literal>();
    for (Literal l : c.literals)
      literals.add(new Literal(l));
    this.weight = c.weight;
  }

  /**
   * Creates a new clause by parsing a string of literals
   * 
   * @param literals
   *          String of literals to parse
   * @param weight
   *          Weight of new clause
   */
  public Clause(String literals, Double weight)
  {
    this.literals = new ArrayList<Literal>();
    this.weight = weight;
    for (String s : literals.split(" ")) {
      if (s.startsWith("!"))
        this.literals.add(new Literal(s.substring(1), true));
      else
        this.literals.add(new Literal(s, false));
    }
  }

  public String toString()
  {
    String result = "(" + weight + ":";
    for (Literal l : literals)
      result += " " + l;
    return result + ")";
  }

  public boolean isHard()
  {
    return weight == Double.POSITIVE_INFINITY;
  }

  /**
   * Returns a clause like the current clause but with all literal change to their opposites, used
   * in building the graph for overestimation
   */
  public Clause allLiteralsNegated()
  {
    Clause res = new Clause(this);
    for (Literal l : res.literals)
      l.neg = !l.neg;
    return res;
  }
}
